i:Id, ds:x:Id fp Type, da:k:Knd fp Type, A:ecl(ds;da), k:Knd, l:IdLnk, tg:Id, n:,
f:(State(ds)Valtype(da;k)da(rcv(l,tg))?Void), es:ES.
(source(l) = i)
 (@i[[A;k sends on l with tag tg [s,v.f(s,v)], at marker n]]
  (es-decls(es;i;ds;da)
   with decls ds 
   with decls da
   sends on l from e 
   include if kind(e) = k  action[[A n]][es-init(es;e);e]
   include then [<tg, f((state when e),val(e))>]
   include else []
   include fi  
   and only these for tags in [tg])) 

latex

Definitions

k sends on l with tag tg [s,v.f(s;v)], at marker n, @i[[x;snd]], as @ bs, concat(ll), tagged-list-messages(s;v;L), Y, reduce(f;k;as), filter(P;l), map(f;as), f(x), x : v, t.2, t.1, mapfilter(f;P;L), f(x)?z, ff, tt, state@i, P  Q, p  q, if b then t else f fi , Valtype(da;k), Knd, Top, {T}, SQType(T), x. t(x), x,y. t(x;y), , t  T, P  Q, P & Q, x(s1,s2), P  Q, P  Q, x:A. B(x), False, A, A c B, with decls ds dasends on l from e include f(e) and only these for tags in tgs, Unit, , x(s),

Lemmas

es-tag wf, l member wf, es-lnk wf, es-val wf, es-sends-iff wf, not functionality wrt iff, es-state-when wf, es-loc wf, pi1 wf, pi2 wf, fpf-single-dom, top wf, fpf-single wf, idlnk-deq wf, product-deq wf, fpf-dom wf, id-deq wf, fpf-sub weakening, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, Knd sq, assert-eq-knd, es-state-subtype, es-loc-init, es-init wf, es-valtype wf, es-isrcv wf, assert wf, es-bact wf, eqtt to assert, bool wf, es-vartype wf, tagged-list-messages wf, es-sends-iff functionality, es-decls-iff, ecl-tags-spec1, Id sq, fpf wf, ecl wf, IdLnk wf, nat wf, rcv wf, Kind-deq wf, Knd wf, fpf-cap wf, decl-state wf, event system wf, lsrc wf, Id wf, ma-valtype wf, msg-spec1 wf, ecl-mng-sends wf